Inference at * 1 
Iof proof for Lemma decidable equal bool:



1. a : 
2. b : 
  Dec(a = b) 

latex

 by ((Unfold `decidable` 0) 
CollapseTHEN (AllBoolInd)) 

latex

C1: 

C1: (no hyps)
C1:   (tt = tt)  ((tt = tt))
C2: 

C2: (no hyps)
C2:   (ff = tt)  ((ff = tt))
C3: 

C3: (no hyps)
C3:   (tt = ff)  ((tt = ff))
C4: 

C4: (no hyps)
C4:   (ff = ff)  ((ff = ff))
C.

Definitions

Dec(P), t  T, Unit, , ff, tt,